(0) Obligation:
Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:
U11(tt) → snd(splitAt(N, XS))
U161(tt) → cons(N)
U171(tt) → head(afterNth(N, XS))
U181(tt) → Y
U191(tt) → pair(nil, XS)
U201(tt) → U202(splitAt(N, XS))
U202(pair(YS, ZS)) → pair(cons(X), ZS)
U21(tt) → X
U211(tt) → XS
U221(tt) → fst(splitAt(N, XS))
U31(tt) → N
and(tt) → X
U101(tt) → U102(isNatural)
U102(tt) → U103(isLNat)
U103(tt) → tt
U111(tt) → U112(isLNat)
U112(tt) → tt
U121(tt) → U122(isNatural)
U122(tt) → tt
U131(tt) → U132(isNatural)
U132(tt) → U133(isLNat)
U133(tt) → tt
U141(tt) → U142(isLNat)
U142(tt) → U143(isLNat)
U143(tt) → tt
U151(tt) → U152(isNatural)
U152(tt) → U153(isLNat)
U153(tt) → tt
U41(tt) → U42(isNatural)
U42(tt) → U43(isLNat)
U43(tt) → tt
U51(tt) → U52(isNatural)
U52(tt) → U53(isLNat)
U53(tt) → tt
U61(tt) → U62(isPLNat)
U62(tt) → tt
U71(tt) → U72(isNatural)
U72(tt) → tt
U81(tt) → U82(isPLNat)
U82(tt) → tt
U91(tt) → U92(isLNat)
U92(tt) → tt
afterNth(N, XS) → U11(and(and(isNatural)))
fst(pair(X, Y)) → U21(and(and(isLNat)))
head(cons(N)) → U31(and(and(isNatural)))
isLNat → tt
isLNat → U41(and(isNaturalKind))
isLNat → U51(and(isNaturalKind))
isLNat → U61(isPLNatKind)
isLNat → U71(isNaturalKind)
isLNat → U81(isPLNatKind)
isLNat → U91(isLNatKind)
isLNat → U101(and(isNaturalKind))
isLNatKind → tt
isLNatKind → and(isNaturalKind)
isLNatKind → isPLNatKind
isLNatKind → isNaturalKind
isLNatKind → isLNatKind
isNatural → tt
isNatural → U111(isLNatKind)
isNatural → U121(isNaturalKind)
isNatural → U131(and(isNaturalKind))
isNaturalKind → tt
isNaturalKind → isLNatKind
isNaturalKind → isNaturalKind
isNaturalKind → and(isNaturalKind)
isPLNat → U141(and(isLNatKind))
isPLNat → U151(and(isNaturalKind))
isPLNatKind → and(isLNatKind)
isPLNatKind → and(isNaturalKind)
natsFrom(N) → U161(and(isNatural))
sel(N, XS) → U171(and(and(isNatural)))
snd(pair(X, Y)) → U181(and(and(isLNat)))
splitAt(0, XS) → U191(and(isLNat))
splitAt(s(N), cons(X)) → U201(and(and(isNatural)))
tail(cons(N)) → U211(and(and(isNatural)))
take(N, XS) → U221(and(and(isNatural)))
(1) CritRuleProof (EQUIVALENT transformation)
The rule U11(tt) → snd(splitAt(N, XS)) contains free variables in its right-hand side. Hence the TRS is not-terminating.
(2) NO